\begin{tabbing}
sendMinimalR\=\{\$a:ut2, \$tg:ut2\}\+
\\[0ex]($T$; $l$; ${\it ds}_{1}$; ${\it ds}_{2}$; $P$; $Q$; $f$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\oplus$(\=[\=at src($l$):\+\+
\\[0ex]action \$a(m) 
\\[0ex]p\=recondition $\lambda$$s$,$m$. $\neg$$P$($s$,$m$) \& ($\forall$$n$:$\mathbb{N}$. $n$$<$$m$ $\Rightarrow$ $P$($s$,$n$))\+
\\[0ex]sends [\$tg,$f$] on link $l$
\-\-\\[0ex]; \=at src(lnk{-}inv($l$)):\+
\\[0ex]action \$a(m) 
\\[0ex]p\=recondition $\lambda$$s$,$m$. $\neg$$Q$($s$,$m$) \& ($\forall$$n$:$\mathbb{N}$. $n$$<$$m$ $\Rightarrow$ $Q$($s$,$n$))\+
\\[0ex]sends [\$tg,$\lambda$$s$,$m$. $m$] on link lnk{-}inv($l$)])
\-\-\-
\end{tabbing}